;;;===========================================================================
;;;
;;; Suspension Equivalence Theorem
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 24/05/10 || End date: 25/05/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "suspension-CC")

(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring-Z *) => *)
 ;; Addition operation ring
 ((addition-ring-Z * *)=> *)
 ;; Product operation ring
 ((product-ring-Z * *) => *)
 ;; Inverse ring
 ((inverse-Z *) => *)
 ;; Zero element ring
 ((zero-element-Z ) => *)
 ;; Unit element ring
 ((unit-Z )=> *)

 ;;--------------------------------------------------
 ;; The homotopy equivalence C1 <<= D1 =>> H1
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; C1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C1 * *) => *)
 ;; Group Operation 
 ((group-operation-C1 * * *) => *)
 ;; Zero element
 ((zero-C1 *) => *)
 ;; External multiplication
 ((external-C1 * * *) => *)
 ;; Inverse element
 ((inverse-C1 * *) => *)

 ;;--------------------------------------------------
 ;; The C1 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-C1 * *) => *)

 ;;--------------------------------------------------
 ;; D1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-D1 * *) => *)
 ;; Group Operation 
 ((group-operation-D1 * * *) => *)
 ;; Zero element
 ((zero-D1 *) => *)
 ;; External multiplication
 ((external-D1 * * *) => *)
 ;; Inverse element
 ((inverse-D1 * *) => *)

 ;;--------------------------------------------------
 ;; The D1 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-D1 * *) => *)

  ;;--------------------------------------------------
 ;; H1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-H1 * *) => *)
 ;; Group Operation 
 ((group-operation-H1 * * *) => *)
 ;; Zero element
 ((zero-H1 *) => *)
 ;; External multiplication
 ((external-H1 * * *) => *)
 ;; Inverse element
 ((inverse-H1 * *) => *)

 ;;--------------------------------------------------
 ;; The H1 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-H1 * *) => *)

 
 ;;--------------------------------------------------
 ;; Morphisms of the homotopy equivalence
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; The lf1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lf1 * *) => *)

 ;;--------------------------------------------------
 ;; The lg1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lg1 * *) => *)


 ;;--------------------------------------------------
 ;; The lh1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lh1 * *) => *)

 ;;--------------------------------------------------
 ;; The rf1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rf1 * *) => *)

 ;;--------------------------------------------------
 ;; The rg1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rg1 * *) => *)


 ;;--------------------------------------------------
 ;; The rh1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rh1 * *) => *)
 
 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring-Z (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring-Z (a b)
	  (+ a b)))

 ;; Product operation ring
 (local (defun product-ring-Z (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse-Z (a)
	  (- a)))

 ;; Zero element ring
 (local (defun zero-element-Z nil
	  0))

 ;; Unit element ring
 (local (defun unit-Z nil
	  1))

 ;;--------------------------------------------------
 ;; C1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C1 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C1 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C1 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C1 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-C1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The C1 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-C1 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; D1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-D1 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-D1 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-D1 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-D1 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-D1 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The D1 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-D1 (n a)
	  (declare (ignore n a))
	  0))

  ;;--------------------------------------------------
 ;; H1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-H1 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-H1 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-H1 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-H1 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-H1 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The H1 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-H1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lf1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lf1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lg1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lg1 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lh1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lh1 (n a)
	  (declare (ignore n a))
	  0))


;;--------------------------------------------------
 ;; The rf1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rf1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The rg1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rg1 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The rh1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rh1 (n a)
	  (declare (ignore n a))
	  0))



  ;;************************************************** 
  ;; Properties
  ;;************************************************** 


(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D1 'group-operation-D1 'zero-D1 'external-D1 'inverse-D1 'd-D1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-C1 'group-operation-C1 'zero-C1 'external-C1 'inverse-C1 'd-C1 )
  'lf1  'lg1  'lh1
  )
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D1 'group-operation-D1 'zero-D1 'external-D1 'inverse-D1 'd-D1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-H1 'group-operation-H1 'zero-H1 'external-H1 'inverse-H1 'd-H1 )
  'rf1  'rg1  'rh1
  ))
 'homotopy-equivalence-1
   )

)


;;==================================================
;; The Suspension definitions
;;==================================================

;;--------------------------------------------------
;; Suspension
;;--------------------------------------------------

(check-chain-complex-p
(chain-complex 'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
	 'inv-C1 'group-operation-C1 'zero-C1 'external-C1 'inverse-C1 'd-C1) 
'C1
:hints '(("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)))))


(defthm c1-help1 (IMPLIES (AND (INV-C1 N A)
              (INV-C1 N B)
              (INV-C1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C1 N A (GROUP-OPERATION-C1 N B C))
		(GROUP-OPERATION-C1 N C (GROUP-OPERATION-C1 N A B))
                )) 
:hints (("Goal" :use ((:instance |C1-is-a-chain-complex|)))))


(defthm c1-help2 (IMPLIES (AND (INV-C1 N A)
              (INV-C1 N B)
              (INV-C1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C1 N A (GROUP-OPERATION-C1 N B C))
		(GROUP-OPERATION-C1 N b (GROUP-OPERATION-C1 N A c))
                )) 
:hints (("Goal" :use ((:instance c1-help1)))))


(defthm c1-help3
	 (IMPLIES (AND (INV-C1 N A) (INTEGERP N))
		  (INV-C1 (+ N -1) (D-C1 N A)))
	 :hints (("Goal" :use ((:instance |C1-is-a-chain-complex|)))))
      
(defthm c1-help4
	 (IMPLIES (AND (INV-C1 N A) (INTEGERP N))
		  (INV-C1 (+ -1 n) (D-C1 N A)))
	 :hints (("Goal" :use ((:instance c1-help3)))))


(definstance-*suspension*
  ((inv-ring inv-ring-Z)
    (addition-ring addition-ring-Z)
    (product-ring product-ring-Z)
    (inverse inverse-Z)
    (zero-element zero-element-Z)
    (unit unit-Z)    
    (inv-C inv-C1) 
    (group-operation-C group-operation-C1)
    (zero-C zero-C1)
    (external-C external-C1)
    (inverse-C inverse-C1)
    (d-C d-C1)    
    )
  "-suspension-C1")



;;--------------------------------------------------
;; Suspension D1
;;--------------------------------------------------


(check-chain-complex-p
(chain-complex 'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
	 'inv-D1 'group-operation-D1 'zero-D1 'external-D1 'inverse-D1 'd-D1) 
'D1
:hints '(("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)))))


(defthm d1-help1 (IMPLIES (AND (INV-D1 N A)
              (INV-D1 N B)
              (INV-D1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D1 N A (GROUP-OPERATION-D1 N B C))
		(GROUP-OPERATION-D1 N C (GROUP-OPERATION-D1 N A B))
                )) 
:hints (("Goal" :use ((:instance |D1-is-a-chain-complex|)))))


(defthm d1-help2 (IMPLIES (AND (INV-D1 N A)
              (INV-D1 N B)
              (INV-D1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D1 N A (GROUP-OPERATION-D1 N B C))
		(GROUP-OPERATION-D1 N b (GROUP-OPERATION-D1 N A c))
                )) 
:hints (("Goal" :use ((:instance d1-help1)))))


(defthm d1-help3
	 (IMPLIES (AND (INV-D1 N A) (INTEGERP N))
		  (INV-D1 (+ N -1) (D-D1 N A)))
	 :hints (("Goal" :use ((:instance |D1-is-a-chain-complex|)))))
      
(defthm d1-help4
	 (IMPLIES (AND (INV-D1 N A) (INTEGERP N))
		  (INV-D1 (+ -1 n) (D-D1 N A)))
	 :hints (("Goal" :use ((:instance d1-help3)))))


(definstance-*suspension*
  ((inv-ring inv-ring-Z)
    (addition-ring addition-ring-Z)
    (product-ring product-ring-Z)
    (inverse inverse-Z)
    (zero-element zero-element-Z)
    (unit unit-Z)
    (inv-C inv-D1) 
    (group-operation-C group-operation-D1)
    (zero-C zero-D1)
    (external-C external-D1)
    (inverse-C inverse-D1)
    (d-C d-D1)    
    )
  "-suspension-D1")



;;--------------------------------------------------
;; Suspension H1
;;--------------------------------------------------

(check-chain-complex-p
(chain-complex 'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
	 'inv-H1 'group-operation-H1 'zero-H1 'external-H1 'inverse-H1 'd-H1) 
'H1
:hints '(("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)))))

(defthm h1-help1 (IMPLIES (AND (INV-H1 N A)
              (INV-H1 N B)
              (INV-H1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-H1 N A (GROUP-OPERATION-H1 N B C))
		(GROUP-OPERATION-H1 N C (GROUP-OPERATION-H1 N A B))
                )) 
:hints (("Goal" :use ((:instance |H1-is-a-chain-complex|)))))


(defthm h1-help2 (IMPLIES (AND (INV-H1 N A)
              (INV-H1 N B)
              (INV-H1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-H1 N A (GROUP-OPERATION-H1 N B C))
		(GROUP-OPERATION-H1 N b (GROUP-OPERATION-H1 N A c))
                )) 
:hints (("Goal" :use ((:instance h1-help1)))))


(defthm h1-help3
	 (IMPLIES (AND (INV-H1 N A) (INTEGERP N))
		  (INV-H1 (+ N -1) (D-H1 N A)))
	 :hints (("Goal" :use ((:instance |H1-is-a-chain-complex|)))))
      
(defthm h1-help4
	 (IMPLIES (AND (INV-H1 N A) (INTEGERP N))
		  (INV-H1 (+ -1 n) (D-H1 N A)))
	 :hints (("Goal" :use ((:instance h1-help3)))))


(definstance-*suspension*
  ((inv-ring inv-ring-Z)
    (addition-ring addition-ring-Z)
    (product-ring product-ring-Z)
    (inverse inverse-Z)
    (zero-element zero-element-Z)
    (unit unit-Z)
    (inv-C inv-H1) 
    (group-operation-C group-operation-H1)
    (zero-C zero-H1)
    (external-C external-H1)
    (inverse-C inverse-H1)
    (d-C d-H1)    
    )
  "-suspension-H1")



;;;--------------------------------------------------
;;; Morphisms of the equivalence
;;;--------------------------------------------------

(defun lf-suspension (n a)
  (inverse-suspension-suspension-c1 n (lf1 (1- n) a))
  )

(defun lg-suspension (n a)
  (inverse-suspension-suspension-d1 n (lg1 (1- n) a))
  )

(defun lh-suspension (n a)
  (inverse-suspension-suspension-d1 (1+ n) (lh1 (1- n) a))
  )

(defun rf-suspension (n a)
  (inverse-suspension-suspension-h1 n (rf1 (1- n) a))
  )

(defun rg-suspension (n a)
  (inverse-suspension-suspension-d1 n (rg1 (1- n) a))
  )

(defun rh-suspension (n a)
  (inverse-suspension-suspension-d1 (1+ n) (rh1 (1- n) a))
  )


;;;--------------------------------------------------
;;; Homotopy Equivalence Suspension
;;;--------------------------------------------------



(in-theory (disable COMMUTATIVITY-OF-+
		    ASSOCIATIVITY-OF-+))


(defthm inv-inverse-lh-d1
  (implies (and (inv-d1 (+ n -1) a)
		(integerp n))
	   (INV-d1 (+ (+ N -1) 1)
                (INVERSE-d1 (+ (+ N -1) 1)
                           (lh1 (+ N -1) A)))))


(defthm inverse-operation=operation-inverse-d1
  (IMPLIES (AND (INV-d1 (+ n -1)  A)
              (INV-d1 (+ n -1) B)
              (INTEGERP N))
         (EQUAL (INVERSE-d1 (+ (+ N -1) 1)
                           (GROUP-OPERATION-d1 (+ (+ N -1) 1)
                                              (lh1 (+ n -1) A)
                                              (lh1 (+ n -1) B)))
                (GROUP-OPERATION-d1 (+ (+ N -1) 1)
                                   (INVERSE-d1 (+ (+ N -1) 1) (lh1 (+ n -1) A))
                                   (INVERSE-d1 (+ (+ N -1) 1)
                                              (lh1 (+ n -1) B)))))
)


(defthm inverse-external-d1
  (IMPLIES (AND (INV-D1 (+ n -1) A)
              (INV-RING-Z R)
              (INTEGERP N))
         (EQUAL (INVERSE-D1 (+ (+ N -1) 1)
                            (EXTERNAL-D1 (+ (+ N -1) 1)
                                         R (LH1 (+ n -1) A)))
                (EXTERNAL-D1 (+ (+ N -1) 1)
                             R
                             (INVERSE-D1 (+ (+ N -1) 1)
                                         (LH1 (+ n -1) A)))))

)


(defthm inverse-zero-d1
  (IMPLIES (INTEGERP N)
         (EQUAL (INVERSE-D1 (+ (+ N -1) 1)
                            (ZERO-D1 (+ (+ N -1) 1)))
                (ZERO-D1 (+ (+ N -1) 1)))))


(defthm inverse-inverse-c1
  (IMPLIES
     (AND (INV-c1 (+ (+ N -1) 1)  A) (INTEGERP N))
     (EQUAL (INVERSE-c1 (+ (+ N -1) 1)
                       (INVERSE-c1 (+ (+ N -1) 1)
                                  a))
            a)))

(defthm lf1-lh1
  (IMPLIES (AND (INV-D1 (+ N -1) GNRT)
              (INTEGERP N))
         (EQUAL (LF1 (+ 1 (+ N -1)) (LH1 (+ N -1) GNRT))
                (ZERO-C1 (+ 1 (+ N -1))))))

(defthm +1+n-1=+n-1+1
  (implies (integerp n)
	   (equal (+ (+ N -1) 1)
		  (+ 1 (+ N -1))))
  :rule-classes nil)

(defthm inverse-lf1-inverse-lh1-zero
  (IMPLIES (AND (INV-D1 (+ N -1) GNRT)
              (INTEGERP N))
         (EQUAL (INVERSE-C1 (+ (+ N -1) 1)
                            (LF1 (+ (+ N -1) 1)
                                 (INVERSE-D1 (+ (+ N -1) 1)
                                             (LH1 (+ N -1) GNRT))))
                (ZERO-C1 (+ (+ N -1) 1))))
  :hints (("Goal" :use (:instance +1+n-1=+n-1+1))))


(defthm inverse-inverse-d1+n-1
  (IMPLIES
     (AND (INV-d1 (+ N -1)  A) (INTEGERP N))
     (EQUAL (INVERSE-d1 (+ N -1)
                       (INVERSE-d1 (+ N -1)
                                  a))
            a))
)


(defthm -1+1-1+n=-1+n
  (implies (integerp n)
	   (equal (+ -1 1 -1 N)
		  (+ -1 N)))
  :rule-classes nil)

(defthm -1-1+1+n=-1+n
  (implies (integerp n)
	   (equal (+ -1 -1 1 N)
		  (+ -1 N)))
  :rule-classes nil)

(defthm +1+n-1-1=+n-1
  (implies (integerp n)
	   (equal (+ 1 (+ (+ N -1) -1))
		  (+ N -1)))
  )

(defthm +n-1-1+1=+n-1
  (implies (integerp n)
	   (equal (+ (+ (+ N -1) -1) 1)
		  (+ N -1)))
  )



(defthm inv-lh1-d-d1
  (implies (and (inv-d1 (+ N -1) gnrt)
		(integerp n))
	   (inv-d1 (+ (+ (+ N -1) -1) 1) (LH1 (+ (+ N -1) -1)
					      (D-D1 (+ N -1) GNRT))))
  :hints (("Goal" :in-theory (disable |+1+N-1-1=+N-1| |+N-1-1+1=+N-1|))))


(defthm inv-lh1-d-d1-2
  (implies (and (inv-d1 (+ N -1) gnrt)
		(integerp n))
	   (inv-d1 (+ N -1) (LH1 (+ (+ N -1) -1)
					      (D-D1 (+ N -1) GNRT))))
  :hints (("Goal" :use ((:instance inv-lh1-d-d1)
			))))

(defthm inv-d-d1+1+n-1
  (implies (and (inv-d1 (+ 1 N -1) a)
		(integerp n))
	   (inv-d1 (+ (+ 1 N -1) -1) (d-d1 (+ 1 N -1) a))))


(defthm +1+n-1-1=+n-1-2
  (implies (integerp n)
	   (equal (+ (+ 1 N -1) -1)
		  (+ N -1)))
  )

(defthm inv-d-d1+1+n-1-2
  (implies (and (inv-d1 (+ 1 N -1) a)
		(integerp n))
	   (inv-d1 (+ N -1) (d-d1 (+ 1 N -1) a)))
  :hints (("Goal"  :use ((:instance inv-d-d1+1+n-1)))))

(defthm +1+n-1=n
  (implies (integerp n)
	   (equal (+ (+ 1 N) -1)
		  n))
  :rule-classes nil)


(defthm inv-inverse-rh1
  (implies (and (inv-d1 (+ n -1) a)
		(integerp n))
	   (INV-D1 (+ (+ N -1) 1)
		   (INVERSE-D1 (+ (+ N -1) 1)
			       (RH1 (+ N -1) A)))))

(defthm inverse-operation=operation-inverse-d1-rh1
  (IMPLIES (AND (INV-d1 (+ n -1)  A)
              (INV-d1 (+ n -1) B)
              (INTEGERP N))
         (EQUAL (INVERSE-d1 (+ (+ N -1) 1)
                           (GROUP-OPERATION-d1 (+ (+ N -1) 1)
                                              (rh1 (+ n -1) A)
                                              (rh1 (+ n -1) B)))
                (GROUP-OPERATION-d1 (+ (+ N -1) 1)
                                   (INVERSE-d1 (+ (+ N -1) 1) (rh1 (+ n -1) A))
                                   (INVERSE-d1 (+ (+ N -1) 1)
                                              (rh1 (+ n -1) B)))))
)



(defthm inverse-external-d1-rh1
  (IMPLIES (AND (INV-D1 (+ n -1) A)
              (INV-RING-Z R)
              (INTEGERP N))
         (EQUAL (INVERSE-D1 (+ (+ N -1) 1)
                            (EXTERNAL-D1 (+ (+ N -1) 1)
                                         R (rH1 (+ n -1) A)))
                (EXTERNAL-D1 (+ (+ N -1) 1)
                             R
                             (INVERSE-D1 (+ (+ N -1) 1)
                                         (rH1 (+ n -1) A)))))

)



(defthm inverse-rf1-inverse-rh1-zero
  (IMPLIES (AND (INV-D1 (+ N -1) GNRT)
              (INTEGERP N))
         (EQUAL (INVERSE-h1 (+ (+ N -1) 1)
                            (rF1 (+ (+ N -1) 1)
                                 (INVERSE-D1 (+ (+ N -1) 1)
                                             (rH1 (+ N -1) GNRT))))
                (ZERO-h1 (+ (+ N -1) 1))))
  :hints (("Goal" :use (:instance +1+n-1=+n-1+1))))

(defthm inverse-inverse-d1+n-1+1-1
  (IMPLIES
     (AND (INV-d1 (+ (+ (+ N -1) 1) 1)  A) (INTEGERP N))
     (EQUAL (INVERSE-d1 (+ (+ (+ N -1) 1) 1)
                       (INVERSE-d1 (+ (+ (+ N -1) 1) 1)
                                  a))
            a))
)



(defthm rh1-rh1
  (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (EQUAL (RH1 (+ N 1) (RH1 N GNRT))
		  (ZERO-D1 (+ (+ N 1) 1))))
:hints (("Goal" :in-theory (enable COMMUTATIVITY-OF-+))))
	   

(defthm inverse-rh1-inverse-rh1-zero
  (IMPLIES (AND (INV-D1 (+ N -1) GNRT)
              (INTEGERP N))
         (EQUAL (INVERSE-d1 (+ (+ (+ N -1) 1) 1)
                            (rh1 (+ (+ N -1) 1)
                                 (INVERSE-D1 (+ (+ N -1) 1)
                                             (rH1 (+ N -1) GNRT))))
                (ZERO-d1 (+ (+ (+ N -1) 1) 1))))
  )



(defthm |+N-1+1=-1+1+N|
  (implies (integerp n)
	   (equal (+ (+ N -1) 1)
		  (+ -1 1 N)))
 :rule-classes nil)

(defthm |+N-1+1+1=-1+1+1+N|
  (implies (integerp n)
	   (equal (+ (+ (+ N -1) 1) 1)
		  (+ -1 1 1 N)))
   :rule-classes nil)


(defthm lh1-lh1-bis
  (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (EQUAL (lH1 (+ N 1) (lH1 N GNRT))
		  (ZERO-D1 (+ (+ N 1) 1))))
:hints (("Goal" :in-theory (enable COMMUTATIVITY-OF-+))))

(defthm inverse-lh1-inverse-lh1-zero
  (IMPLIES (AND (INV-D1 (+ N -1) GNRT)
              (INTEGERP N))
         (EQUAL (INVERSE-d1 (+ (+ (+ N -1) 1) 1)
                            (lh1 (+ (+ N -1) 1)
                                 (INVERSE-D1 (+ (+ N -1) 1)
                                             (lH1 (+ N -1) GNRT))))
                (ZERO-d1 (+ (+ (+ N -1) 1) 1))))
 )


(defthm +1-1+n=-1+1+n
  (implies (integerp n)
	   (equal (+ 1 -1 n)
		  (+ -1 1 n)))
  :rule-classes nil)


(in-theory (disable COMMUTATIVITY-OF-+
		    ASSOCIATIVITY-OF-+))


(defthm inv-rh1-d-d1
  (implies (and (inv-d1 (+ n -1) gnrt)
		(integerp n))
	   (inv-d1 (+ (+ (+ N -1) -1) 1)
		   (RH1 (+ (+ N -1) -1)
			(D-D1 (+ N -1) GNRT))))
  :hints (("Goal" :in-theory (disable |+N-1-1+1=+N-1|))))


(defthm inv-rh1-d-d1-b
  (implies (and (inv-d1 (+ n -1) gnrt)
		(integerp n))
	   (inv-d1 (+ N -1)
		   (RH1 (+ (+ N -1) -1)
			(D-D1 (+ N -1) GNRT))))
  :hints (("Goal" :use (:instance inv-rh1-d-d1))))
 

(defthm rh1+d-d1orh1=id-rg1orf1-help
  (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1 N (RH1 (+ N -1) (D-D1 N GNRT))
				(D-D1 (+ N 1) (RH1 N GNRT)))
	    (GROUP-OPERATION-D1 N GNRT
				(INVERSE-D1 N (RG1 N (RF1 N GNRT)))))
	   )
  :hints (("Goal" :in-theory (enable COMMUTATIVITY-OF-+))))

(defthm rh1+d-d1orh1=id-rg1orf1
  (implies (and (inv-d1 (+ n -1) gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1
	     (+ N -1)
	     (INVERSE-D1 (+ (+ (+ n -1) -1) 1)
			 (INVERSE-D1 (+ (+ (+ n -1) -1) 1)
				     (RH1 (+ (+ n -1) -1) (D-D1 (+ n -1) GNRT))))
	     (INVERSE-D1 (+ (+ (+ n -1) 1) -1)
			 (D-D1 (+ (+ n -1) 1)
			       (INVERSE-D1 (+ (+ n -1) 1)
					   (RH1 (+ n -1) GNRT)))))
	    (GROUP-OPERATION-D1
	     (+ n -1)
	     GNRT
	     (INVERSE-D1 (+ n -1)
			 (INVERSE-D1 (+ n -1)
				     (INVERSE-D1 (+ n -1)
						 (RG1 (+ n -1) (RF1 (+ n -1) GNRT)))))))
	   

	   ))



(defthm inv-lh1-d-d1-b
  (implies (and (inv-d1 (+ n -1) gnrt)
		(integerp n))
	   (inv-d1 (+ N -1)
		   (lH1 (+ (+ N -1) -1)
			(D-D1 (+ N -1) GNRT))))
  :hints (("Goal" :use (:instance inv-lh1-d-d1))))
 

(defthm lh1+d-d1olh1=id-lg1olf1-help
  (implies (and (inv-d1 n gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1 N (lH1 (+ N -1) (D-D1 N GNRT))
				(D-D1 (+ N 1) (lH1 N GNRT)))
	    (GROUP-OPERATION-D1 N GNRT
				(INVERSE-D1 N (lG1 N (lF1 N GNRT)))))
	   )
  :hints (("Goal" :in-theory (enable COMMUTATIVITY-OF-+))))

(defthm lh1+d-d1olh1=id-lg1olf1
  (implies (and (inv-d1 (+ n -1) gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1
	     (+ N -1)
	     (INVERSE-D1 (+ (+ (+ n -1) -1) 1)
			 (INVERSE-D1 (+ (+ (+ n -1) -1) 1)
				     (lH1 (+ (+ n -1) -1) (D-D1 (+ n -1) GNRT))))
	     (INVERSE-D1 (+ (+ (+ n -1) 1) -1)
			 (D-D1 (+ (+ n -1) 1)
			       (INVERSE-D1 (+ (+ n -1) 1)
					   (lH1 (+ n -1) GNRT)))))
	    (GROUP-OPERATION-D1
	     (+ n -1)
	     GNRT
	     (INVERSE-D1 (+ n -1)
			 (INVERSE-D1 (+ n -1)
				     (INVERSE-D1 (+ n -1)
						 (lG1 (+ n -1) (lF1 (+ n -1) GNRT)))))))
	   

	   ))
 


(in-theory (enable COMMUTATIVITY-OF-+))


(defthm |-1+N=+N-1|
  (equal (+ -1 N) (+ n -1))
  :rule-classes nil)


(defthm -1+1-1+n=+n-1-1+1
  (equal (+ -1 1 -1 N)
	 (+ (+ (+ n -1) -1) 1))
  :rule-classes nil)

(defthm -1-1+1+n=+n-1-1+1
  (equal (+ -1 -1 1 N)
	 (+ (+ (+ n -1) -1) 1))
  :rule-classes nil)

(defthm -1+1+n=+n-1+1
    (equal (+ -1 1 N)
	(+ (+ n -1) 1) )
  :rule-classes nil)

(defthm -1+n-1=+n-1-1
    (equal (+ -1 N -1)
	(+ (+ n -1) -1) )
  :rule-classes nil)

(defthm +n-1-1+1=+n-1+1-1
  (equal (+ (+ (+ N -1) -1) 1)
	 (+ (+ (+ N -1) 1) -1))
  :rule-classes nil)


(defthm inverse-d1-rule
  (implies (integerp n)
	   (equal (INVERSE-D1 (+ (+ (+ N -1) -1) 1)
                                   a)
		  (INVERSE-D1 (+ (+ (+ N -1) 1) -1)
                                   a)
))
  :hints (("Goal" :use (:instance |+N-1-1+1=+N-1+1-1|))))


(defthm lh1+d-d1olh1=id-lg1olf1-bis
  (implies (and (inv-d1 (+ -1 n) gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1
	     (+ -1 N)
	     (INVERSE-D1 (+ -1 1 -1 N)
			 (INVERSE-D1 (+ -1 1 -1 N)
				     (lH1 (+ -1 -1 N) (D-D1 (+ -1 N) GNRT))))
	     (INVERSE-D1 (+ -1 -1 1 N)
			 (D-D1 (+ -1 1 N)
			       (INVERSE-D1 (+ -1 1 N)
					   (lH1 (+ -1 N) GNRT)))))
	    (GROUP-OPERATION-D1
	     (+ -1 N)
	     GNRT
	     (INVERSE-D1 (+ -1 N)
			 (INVERSE-D1 (+ -1 N)
				     (INVERSE-D1 (+ -1 N)
						 (lG1 (+ -1 N) (lF1 (+ -1 N) GNRT)))))))
	   
	   )
  :hints (("Goal" :in-theory (disable COMMUTATIVITY-OF-+
				      |+N-1-1+1=+N-1|
				      D1-HELP3
				      |D1-is-a-chain-complex|
				      |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|
				      INVERSE-INVERSE-D1+N-1)
	   :use ((:instance |-1+N=+N-1|)
		 (:instance |-1+1-1+N=+N-1-1+1|)
		 (:instance |-1-1+1+N=+N-1-1+1|)
		 (:instance |-1+1+N=+N-1+1|)
		 (:instance |-1+N-1=+N-1-1|)
		 (:instance inverse-d1-rule)
		 (:instance lh1+d-d1olh1=id-lg1olf1)))))

(defthm rh1+d-d1orh1=id-rg1orf1-bis
  (implies (and (inv-d1 (+ -1 n) gnrt)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-D1
	     (+ -1 N)
	     (INVERSE-D1 (+ -1 1 -1 N)
			 (INVERSE-D1 (+ -1 1 -1 N)
				     (RH1 (+ -1 -1 N) (D-D1 (+ -1 N) GNRT))))
	     (INVERSE-D1 (+ -1 -1 1 N)
			 (D-D1 (+ -1 1 N)
			       (INVERSE-D1 (+ -1 1 N)
					   (RH1 (+ -1 N) GNRT)))))
	    (GROUP-OPERATION-D1
	     (+ -1 N)
	     GNRT
	     (INVERSE-D1 (+ -1 N)
			 (INVERSE-D1 (+ -1 N)
				     (INVERSE-D1 (+ -1 N)
						 (RG1 (+ -1 N) (RF1 (+ -1 N) GNRT)))))))
	   
	   )
  :hints (("Goal" :in-theory (disable COMMUTATIVITY-OF-+
				      |+N-1-1+1=+N-1|
				      D1-HELP3
				      |D1-is-a-chain-complex|
				      |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|
				      INVERSE-INVERSE-D1+N-1)
	   :use ((:instance |-1+N=+N-1|)
		 (:instance |-1+1-1+N=+N-1-1+1|)
		 (:instance |-1-1+1+N=+N-1-1+1|)
		 (:instance |-1+1+N=+N-1+1|)
		 (:instance |-1+N-1=+N-1-1|)
		 (:instance inverse-d1-rule)
		 (:instance rh1+d-d1orh1=id-rg1orf1)))))



(defthm inverse-lh1-inverse-lh1-zero-bis
  (IMPLIES (AND (INV-D1 (+ -1 n) GNRT)
              (INTEGERP N))
         (EQUAL (INVERSE-D1 (+ -1 1 1 N)
                   (lH1 (+ -1 1 N)
                        (INVERSE-D1 (+ -1 1 N)
                                    (lH1 (+ -1 N) GNRT))))
       (ZERO-D1 (+ -1 1 1 N))))
  :hints (("Goal" :use ((:instance inverse-lh1-inverse-lh1-zero)
			(:instance |+N-1+1=-1+1+N|)
			(:instance |+N-1+1+1=-1+1+1+N|)
			))))


(defthm inverse-rh1-inverse-rh1-zero-bis
  (IMPLIES (AND (INV-D1 (+ -1 n) GNRT)
              (INTEGERP N))
         (EQUAL (INVERSE-D1 (+ -1 1 1 N)
                   (RH1 (+ -1 1 N)
                        (INVERSE-D1 (+ -1 1 N)
                                    (RH1 (+ -1 N) GNRT))))
       (ZERO-D1 (+ -1 1 1 N))))
  :hints (("Goal" :use ((:instance inverse-rh1-inverse-rh1-zero)
			(:instance |+N-1+1=-1+1+N|)
			(:instance |+N-1+1+1=-1+1+1+N|)
			))))

(defthm inverse-rf1-inverse-rh1-zero-bis
  (IMPLIES (AND (INV-D1 (+ -1 N) GNRT)
              (INTEGERP N))
         (EQUAL (INVERSE-h1 (+ -1 1 N)
                            (rF1 (+ -1 1 N)
                                 (INVERSE-D1 (+ -1 1 N)
                                             (rH1 (+ -1 N) GNRT))))
                (ZERO-h1 (+ -1 1 N))))
  :hints (("Goal" :use ((:instance inverse-rf1-inverse-rh1-zero)
		      (:instance +1-1+n=-1+1+n)))))


(defthm inverse-external-d1-rh1-bis
  (IMPLIES (AND (INV-D1 (+ -1 N) A)
              (INV-RING-Z R)
              (INTEGERP N))
         (EQUAL (INVERSE-D1 (+ -1 1 N)
                            (EXTERNAL-D1 (+ 1 -1 N)
                                         R (rH1 (+ -1 N) A)))
                (EXTERNAL-D1 (+ -1 1 N)
                             R
                             (INVERSE-D1 (+ -1 1 N)
                                         (rH1 (+ -1 N) A)))))
:hints (("Goal" :use ((:instance inverse-external-d1-rh1)
		      (:instance +1-1+n=-1+1+n)))))

(defthm inverse-operation=operation-inverse-d1-rh1-bis
  (IMPLIES (AND (INV-d1 (+ -1 n)  A)
              (INV-d1 (+ -1 n) B)
              (INTEGERP N))
         (EQUAL (INVERSE-d1 (+ -1 1 N)
                           (GROUP-OPERATION-d1 (+ 1 -1 N)
                                              (rh1 (+ -1 n) A)
                                              (rh1 (+ -1 n) B)))
                (GROUP-OPERATION-d1 (+ -1 1 N)
                                   (INVERSE-d1 (+ -1 1 N) (rh1 (+ -1 n) A))
                                   (INVERSE-d1 (+ -1 1 N)
                                              (rh1 (+ -1 n) B)))))
:hints (("Goal" :use ((:instance inverse-operation=operation-inverse-d1-rh1)
		      (:instance +1-1+n=-1+1+n)))))


(defthm inv-inverse-rh1-bis
  (implies (and (inv-d1 (+ -1 n) a)
		(integerp n))
	   (INV-D1 (+ -1 1 N)
		   (INVERSE-D1 (+ -1 1 N)
			       (RH1 (+ -1 N) A))))
  :hints (("Goal" :use ((:instance inv-inverse-rh1)
			(:instance |+1-1+N=-1+1+N|)))))



(defthm inv-inverse-lh-d1-bis
  (implies (and (inv-d1 (+ -1 n) a)
		(integerp n))
	   (INV-d1(+ -1 1 N)
                (INVERSE-d1 (+ -1 1 N)
                           (lh1 (+ -1 n) A))))
  :hints (("Goal" :use ((:instance inv-inverse-lh-d1)
			(:instance +1-1+n=-1+1+n)))))

(defthm inverse-operation=operation-inverse-d1-bis
  (IMPLIES (AND (INV-d1 (+ -1 n)  A)
              (INV-d1 (+ -1 n) B)
              (INTEGERP N))
         (EQUAL (INVERSE-d1 (+ -1 1 N)
                           (GROUP-OPERATION-d1 (+ 1 -1 N)
                                              (lh1 (+ -1 n) A)
                                              (lh1 (+ -1 n) B)))
                (GROUP-OPERATION-d1 (+ -1 1 N)
                                   (INVERSE-d1 (+ -1 1 N) (lh1 (+ -1 n) A))
                                   (INVERSE-d1 (+ -1 1 N)
                                              (lh1 (+ -1 n) B)))))
:hints (("Goal" :use ((:instance inverse-operation=operation-inverse-d1)
		      (:instance +1-1+n=-1+1+n)))))



(defthm inverse-external-d1-bis
  (IMPLIES (AND (INV-D1 (+ -1 N) A)
              (INV-RING-Z R)
              (INTEGERP N))
         (EQUAL (INVERSE-D1 (+ -1 1 N)
                            (EXTERNAL-D1 (+ 1 -1 N)
                                         R (LH1 (+ -1 N) A)))
                (EXTERNAL-D1 (+ -1 1 N)
                             R
                             (INVERSE-D1 (+ -1 1 N)
                                         (LH1 (+ -1 N) A)))))
:hints (("Goal" :use ((:instance inverse-external-d1)
		      (:instance +1-1+n=-1+1+n)))))


(defthm inverse-zero-d1-bis
  (IMPLIES (INTEGERP N)
         (EQUAL (INVERSE-D1 (+ -1 1 N)
                            (ZERO-D1 (+ 1 -1 N)))
                (ZERO-D1 (+ -1 1 N))))
  :hints (("Goal" :use ((:instance inverse-zero-d1)
		      (:instance +1-1+n=-1+1+n)))))

(defthm inverse-inverse-d1
  (IMPLIES (AND (INV-D1 (+ -1 N) A) (INTEGERP N))
         (EQUAL (INVERSE-D1 (+ -1 1 N)
                            (INVERSE-D1 (+ 1 -1 N)
                                        (LH1 (+ -1 N) A)))
                (INVERSE-D1 (+ -1 1 N)
                            (INVERSE-D1 (+ -1 1 N)
                                        (LH1 (+ -1 N) A)))))
  :hints (("Goal" :use ((:instance +1-1+n=-1+1+n)))))


(defthm inverse-inverse-d1-rh1
  (IMPLIES (AND (INV-D1 (+ -1 N) A) (INTEGERP N))
         (EQUAL (INVERSE-D1 (+ -1 1 N)
                            (INVERSE-D1 (+ 1 -1 N)
                                        (rH1 (+ -1 N) A)))
                (INVERSE-D1 (+ -1 1 N)
                            (INVERSE-D1 (+ -1 1 N)
                                        (rH1 (+ -1 N) A)))))
  :hints (("Goal" :use ((:instance +1-1+n=-1+1+n)))))


(defthm inverse-lf1-inverse-lh1-zero-bis
  (IMPLIES (AND (INV-D1 (+ -1 N) GNRT)
              (INTEGERP N))
         (EQUAL (INVERSE-C1 (+ -1 1 N)
                            (LF1 (+ -1 1 N)
                                 (INVERSE-D1 (+ -1 1 N)
                                             (LH1 (+ -1 N) GNRT))))
                (ZERO-C1 (+ -1 1 N))))
  :hints (("Goal" :use ((:instance inverse-lf1-inverse-lh1-zero)
		      (:instance +1-1+n=-1+1+n)))))


(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-suspension-suspension-D1 'group-suspension-suspension-operation-D1 'zero-suspension-suspension-D1 
   'external-suspension-suspension-D1 'inverse-suspension-suspension-D1 'd-suspension-suspension-D1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-suspension-suspension-C1 'group-operation-suspension-suspension-C1 'zero-suspension-suspension-C1 'external-suspension-suspension-C1 'inverse-suspension-suspension-C1 'd-suspension-suspension-C1 )
  'lf-suspension  'lg-suspension  'lh-suspension
  )
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-suspension-suspension-D1 'group-operation-suspension-suspension-D1 'zero-suspension-suspension-D1 'external-suspension-suspension-D1 'inverse-suspension-suspension-D1 'd-suspension-suspension-D1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-suspension-suspension-H1 'group-operation-suspension-suspension-H1 'zero-suspension-suspension-H1 'external-suspension-suspension-H1 'inverse-suspension-suspension-H1 'd-suspension-suspension-H1 )
  'rf-suspension  'rg-suspension  'rh-suspension
  ))
 'homotopy-equivalence-suspension  
   )

;;;===========================================================================
;;;
;;; End of the proof of the Suspension Equivalence Theorem
;;;
;;;===========================================================================

;;;----------------------------------------------------------------------------
;;; 
;;; Defining the generic theory:
;;;
;;;----------------------------------------------------------------------------


(include-book "generic-theory")


#|
(get-event-lst 
 '(inv-suspension-suspension-c1 group-operation-suspension-suspension-c1 zero-suspension-suspension-c1 external-suspension-suspension-c1 inverse-suspension-suspension-c1 d-suspension-suspension-c1
   inv-suspension-suspension-d1 group-operation-suspension-suspension-d1 zero-suspension-suspension-d1 external-suspension-suspension-d1 inverse-suspension-suspension-d1 d-suspension-suspension-d1 
   inv-suspension-suspension-h1 group-operation-suspension-suspension-h1 zero-suspension-suspension-h1 external-suspension-suspension-h1 inverse-suspension-suspension-h1 d-suspension-suspension-h1
   lf-suspension  lg-suspension  lh-suspension rf-suspension rg-suspension rh-suspension
   |HOMOTOPY-EQUIVALENCE-SUSPENSION-is-an-homotopy-equivalence|
   )
 )
|#


(defconst *suspension-reduction-theorem*
  '((DEFUN INV-SUSPENSION-SUSPENSION-C1 (N A)
        (INV-C1 (1- N) A))
 (DEFUN GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
        (N A B)
        (GROUP-OPERATION-C1 (1- N) A B))
 (DEFUN ZERO-SUSPENSION-SUSPENSION-C1 (N)
        (ZERO-C1 (1- N)))
 (DEFUN EXTERNAL-SUSPENSION-SUSPENSION-C1
        (N A B)
        (EXTERNAL-C1 (1- N) A B))
 (DEFUN INVERSE-SUSPENSION-SUSPENSION-C1 (N A)
        (INVERSE-C1 (1- N) A))
 (DEFUN D-SUSPENSION-SUSPENSION-C1 (N A)
        (INVERSE-C1 (1- (1- N))
                    (D-C1 (1- N) A)))
 (DEFUN INV-SUSPENSION-SUSPENSION-D1 (N A)
        (INV-D1 (1- N) A))
 (DEFUN GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
        (N A B)
        (GROUP-OPERATION-D1 (1- N) A B))
 (DEFUN ZERO-SUSPENSION-SUSPENSION-D1 (N)
        (ZERO-D1 (1- N)))
 (DEFUN EXTERNAL-SUSPENSION-SUSPENSION-D1
        (N A B)
        (EXTERNAL-D1 (1- N) A B))
 (DEFUN INVERSE-SUSPENSION-SUSPENSION-D1 (N A)
        (INVERSE-D1 (1- N) A))
 (DEFUN D-SUSPENSION-SUSPENSION-D1 (N A)
        (INVERSE-D1 (1- (1- N))
                    (D-D1 (1- N) A)))
 (DEFUN INV-SUSPENSION-SUSPENSION-H1 (N A)
        (INV-H1 (1- N) A))
 (DEFUN GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
        (N A B)
        (GROUP-OPERATION-H1 (1- N) A B))
 (DEFUN ZERO-SUSPENSION-SUSPENSION-H1 (N)
        (ZERO-H1 (1- N)))
 (DEFUN EXTERNAL-SUSPENSION-SUSPENSION-H1
        (N A B)
        (EXTERNAL-H1 (1- N) A B))
 (DEFUN INVERSE-SUSPENSION-SUSPENSION-H1 (N A)
        (INVERSE-H1 (1- N) A))
 (DEFUN D-SUSPENSION-SUSPENSION-H1 (N A)
        (INVERSE-H1 (1- (1- N))
                    (D-H1 (1- N) A)))
 (DEFUN LF-SUSPENSION (N A)
        (INVERSE-SUSPENSION-SUSPENSION-C1 N (LF1 (1- N) A)))
 (DEFUN LG-SUSPENSION (N A)
        (INVERSE-SUSPENSION-SUSPENSION-D1 N (LG1 (1- N) A)))
 (DEFUN LH-SUSPENSION (N A)
        (INVERSE-SUSPENSION-SUSPENSION-D1 (1+ N)
                                          (LH1 (1- N) A)))
 (DEFUN RF-SUSPENSION (N A)
        (INVERSE-SUSPENSION-SUSPENSION-H1 N (RF1 (1- N) A)))
 (DEFUN RG-SUSPENSION (N A)
        (INVERSE-SUSPENSION-SUSPENSION-D1 N (RG1 (1- N) A)))
 (DEFUN RH-SUSPENSION (N A)
        (INVERSE-SUSPENSION-SUSPENSION-D1 (1+ N)
                                          (RH1 (1- N) A)))
 (DEFTHM
  |HOMOTOPY-EQUIVALENCE-SUSPENSION-is-an-homotopy-equivalence|
  (AND
   (AND
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-SUSPENSION-SUSPENSION-D1 N B)
                 (INV-SUSPENSION-SUSPENSION-D1 N C)
                 (INTEGERP N))
            (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                        C)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N A
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N B C))))
       (INV-SUSPENSION-SUSPENSION-D1 N (ZERO-SUSPENSION-SUSPENSION-D1 N))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N A (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (INVERSE-SUSPENSION-SUSPENSION-D1 N A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                            (ZERO-SUSPENSION-SUSPENSION-D1 N)))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1 N A)
                       B))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N A
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N B A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N R
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A)
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R B))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (ADDITION-RING-Z S R)
                                                      A)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N S A)
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (PRODUCT-RING-Z S R)
                                                      A)
                   (EXTERNAL-SUSPENSION-SUSPENSION-D1
                        N S
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (UNIT-Z)
                                                          A)
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N (INVERSE-SUSPENSION-SUSPENSION-D1 N A)
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N B))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N S A))
                       (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N S
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N S (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N))))
      (AND
       (AND
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                  (INTEGERP N))
             (INV-SUSPENSION-SUSPENSION-D1 (+ N -1)
                                           (D-SUSPENSION-SUSPENSION-D1 N A)))
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                  (INV-SUSPENSION-SUSPENSION-D1 N B)
                  (INTEGERP N))
             (EQUAL (D-SUSPENSION-SUSPENSION-D1
                         N
                         (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                         (+ N -1)
                         (D-SUSPENSION-SUSPENSION-D1 N A)
                         (D-SUSPENSION-SUSPENSION-D1 N B))))
        (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-SUSPENSION-SUSPENSION-D1
                             N
                             (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1
                             (+ N -1)
                             R (D-SUSPENSION-SUSPENSION-D1 N A))))
        (IMPLIES
         (INTEGERP N)
         (EQUAL
             (D-SUSPENSION-SUSPENSION-D1 N (ZERO-SUSPENSION-SUSPENSION-D1 N))
             (ZERO-SUSPENSION-SUSPENSION-D1 (+ N -1))))
        (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INTEGERP N))
         (EQUAL
          (D-SUSPENSION-SUSPENSION-D1 N
                                      (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
          (INVERSE-SUSPENSION-SUSPENSION-D1
               (+ N -1)
               (D-SUSPENSION-SUSPENSION-D1 N A)))))
       (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INTEGERP N))
         (EQUAL (D-SUSPENSION-SUSPENSION-D1 (1- N)
                                            (D-SUSPENSION-SUSPENSION-D1 N A))
                (ZERO-SUSPENSION-SUSPENSION-D1 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-C1
                     N
                     (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B)))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                 (INV-SUSPENSION-SUSPENSION-C1 N B)
                 (INV-SUSPENSION-SUSPENSION-C1 N C)
                 (INTEGERP N))
            (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                        N
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B)
                        C)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                        N A
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N B C))))
       (INV-SUSPENSION-SUSPENSION-C1 N (ZERO-SUSPENSION-SUSPENSION-C1 N))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-C1
                     N
                     (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                            N A (ZERO-SUSPENSION-SUSPENSION-C1 N))
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-C1
                     N
                     (INVERSE-SUSPENSION-SUSPENSION-C1 N A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B)
                            (ZERO-SUSPENSION-SUSPENSION-C1 N)))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-C1 N A)
                       B))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                            N A
                            (INVERSE-SUSPENSION-SUSPENSION-C1 N A))
                       (ZERO-SUSPENSION-SUSPENSION-C1 N)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B)
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N B A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1
                            N R
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A)
                            (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R B))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1 N (ADDITION-RING-Z S R)
                                                      A)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                        N
                        (EXTERNAL-SUSPENSION-SUSPENSION-C1 N S A)
                        (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1 N (PRODUCT-RING-Z S R)
                                                      A)
                   (EXTERNAL-SUSPENSION-SUSPENSION-C1
                        N S
                        (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1 N (UNIT-Z)
                                                          A)
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-C1
                            N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                            N (INVERSE-SUSPENSION-SUSPENSION-C1 N A)
                            (INVERSE-SUSPENSION-SUSPENSION-C1 N B))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-C1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-C1 N S A))
                       (EXTERNAL-SUSPENSION-SUSPENSION-C1
                            N S
                            (INVERSE-SUSPENSION-SUSPENSION-C1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-C1
                            N (ZERO-SUSPENSION-SUSPENSION-C1 N))
                       (ZERO-SUSPENSION-SUSPENSION-C1 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1
                            N S (ZERO-SUSPENSION-SUSPENSION-C1 N))
                       (ZERO-SUSPENSION-SUSPENSION-C1 N))))
      (AND
       (AND
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                  (INTEGERP N))
             (INV-SUSPENSION-SUSPENSION-C1 (+ N -1)
                                           (D-SUSPENSION-SUSPENSION-C1 N A)))
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                  (INV-SUSPENSION-SUSPENSION-C1 N B)
                  (INTEGERP N))
             (EQUAL (D-SUSPENSION-SUSPENSION-C1
                         N
                         (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                         (+ N -1)
                         (D-SUSPENSION-SUSPENSION-C1 N A)
                         (D-SUSPENSION-SUSPENSION-C1 N B))))
        (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-SUSPENSION-SUSPENSION-C1
                             N
                             (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A))
                        (EXTERNAL-SUSPENSION-SUSPENSION-C1
                             (+ N -1)
                             R (D-SUSPENSION-SUSPENSION-C1 N A))))
        (IMPLIES
         (INTEGERP N)
         (EQUAL
             (D-SUSPENSION-SUSPENSION-C1 N (ZERO-SUSPENSION-SUSPENSION-C1 N))
             (ZERO-SUSPENSION-SUSPENSION-C1 (+ N -1))))
        (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
              (INTEGERP N))
         (EQUAL
          (D-SUSPENSION-SUSPENSION-C1 N
                                      (INVERSE-SUSPENSION-SUSPENSION-C1 N A))
          (INVERSE-SUSPENSION-SUSPENSION-C1
               (+ N -1)
               (D-SUSPENSION-SUSPENSION-C1 N A)))))
       (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
              (INTEGERP N))
         (EQUAL (D-SUSPENSION-SUSPENSION-C1 (1- N)
                                            (D-SUSPENSION-SUSPENSION-C1 N A))
                (ZERO-SUSPENSION-SUSPENSION-C1 (1- (1- N)))))))
     (AND
      (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                    (INTEGERP N))
               (INV-SUSPENSION-SUSPENSION-C1 N (LF-SUSPENSION N A)))
      (IMPLIES
        (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
             (INV-SUSPENSION-SUSPENSION-D1 N B)
             (INTEGERP N))
        (EQUAL
             (LF-SUSPENSION N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
             (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N (LF-SUSPENSION N A)
                                                       (LF-SUSPENSION N B))))
      (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INV-RING-Z R)
              (INTEGERP N))
         (EQUAL (LF-SUSPENSION N
                               (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))
                (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R (LF-SUSPENSION N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (LF-SUSPENSION N (ZERO-SUSPENSION-SUSPENSION-D1 N))
                      (ZERO-SUSPENSION-SUSPENSION-C1 N)))
      (IMPLIES
           (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                (INTEGERP N))
           (EQUAL (LF-SUSPENSION N
                                 (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
                  (INVERSE-SUSPENSION-SUSPENSION-C1 N (LF-SUSPENSION N A)))))
     (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                   (INTEGERP N))
              (EQUAL (D-SUSPENSION-SUSPENSION-C1 N (LF-SUSPENSION N A))
                     (LF-SUSPENSION (1- N)
                                    (D-SUSPENSION-SUSPENSION-D1 N A)))))
    (AND
     (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                   (INTEGERP N))
              (INV-SUSPENSION-SUSPENSION-D1 (+ N 1)
                                            (LH-SUSPENSION N A)))
     (IMPLIES
      (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
           (INV-SUSPENSION-SUSPENSION-D1 N B)
           (INTEGERP N))
      (EQUAL (LH-SUSPENSION N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
             (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 (+ N 1)
                                                       (LH-SUSPENSION N A)
                                                       (LH-SUSPENSION N B))))
     (IMPLIES
          (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (LH-SUSPENSION N
                                (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))
                 (EXTERNAL-SUSPENSION-SUSPENSION-D1 (+ N 1)
                                                    R (LH-SUSPENSION N A))))
     (IMPLIES (INTEGERP N)
              (EQUAL (LH-SUSPENSION N (ZERO-SUSPENSION-SUSPENSION-D1 N))
                     (ZERO-SUSPENSION-SUSPENSION-D1 (+ N 1))))
     (IMPLIES
          (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
               (INTEGERP N))
          (EQUAL (LH-SUSPENSION N
                                (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
                 (INVERSE-SUSPENSION-SUSPENSION-D1 (+ N 1)
                                                   (LH-SUSPENSION N A)))))
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-C1
                     N
                     (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B)))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                 (INV-SUSPENSION-SUSPENSION-C1 N B)
                 (INV-SUSPENSION-SUSPENSION-C1 N C)
                 (INTEGERP N))
            (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                        N
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B)
                        C)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                        N A
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N B C))))
       (INV-SUSPENSION-SUSPENSION-C1 N (ZERO-SUSPENSION-SUSPENSION-C1 N))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-C1
                     N
                     (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                            N A (ZERO-SUSPENSION-SUSPENSION-C1 N))
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-C1
                     N
                     (INVERSE-SUSPENSION-SUSPENSION-C1 N A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B)
                            (ZERO-SUSPENSION-SUSPENSION-C1 N)))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-C1 N A)
                       B))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                            N A
                            (INVERSE-SUSPENSION-SUSPENSION-C1 N A))
                       (ZERO-SUSPENSION-SUSPENSION-C1 N)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B)
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N B A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1
                            N R
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A)
                            (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R B))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1 N (ADDITION-RING-Z S R)
                                                      A)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                        N
                        (EXTERNAL-SUSPENSION-SUSPENSION-C1 N S A)
                        (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1 N (PRODUCT-RING-Z S R)
                                                      A)
                   (EXTERNAL-SUSPENSION-SUSPENSION-C1
                        N S
                        (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1 N (UNIT-Z)
                                                          A)
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-SUSPENSION-SUSPENSION-C1 N B)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-C1
                            N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                            N (INVERSE-SUSPENSION-SUSPENSION-C1 N A)
                            (INVERSE-SUSPENSION-SUSPENSION-C1 N B))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-C1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-C1 N S A))
                       (EXTERNAL-SUSPENSION-SUSPENSION-C1
                            N S
                            (INVERSE-SUSPENSION-SUSPENSION-C1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-C1
                            N (ZERO-SUSPENSION-SUSPENSION-C1 N))
                       (ZERO-SUSPENSION-SUSPENSION-C1 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-C1
                            N S (ZERO-SUSPENSION-SUSPENSION-C1 N))
                       (ZERO-SUSPENSION-SUSPENSION-C1 N))))
      (AND
       (AND
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                  (INTEGERP N))
             (INV-SUSPENSION-SUSPENSION-C1 (+ N -1)
                                           (D-SUSPENSION-SUSPENSION-C1 N A)))
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                  (INV-SUSPENSION-SUSPENSION-C1 N B)
                  (INTEGERP N))
             (EQUAL (D-SUSPENSION-SUSPENSION-C1
                         N
                         (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1
                         (+ N -1)
                         (D-SUSPENSION-SUSPENSION-C1 N A)
                         (D-SUSPENSION-SUSPENSION-C1 N B))))
        (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-SUSPENSION-SUSPENSION-C1
                             N
                             (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A))
                        (EXTERNAL-SUSPENSION-SUSPENSION-C1
                             (+ N -1)
                             R (D-SUSPENSION-SUSPENSION-C1 N A))))
        (IMPLIES
         (INTEGERP N)
         (EQUAL
             (D-SUSPENSION-SUSPENSION-C1 N (ZERO-SUSPENSION-SUSPENSION-C1 N))
             (ZERO-SUSPENSION-SUSPENSION-C1 (+ N -1))))
        (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
              (INTEGERP N))
         (EQUAL
          (D-SUSPENSION-SUSPENSION-C1 N
                                      (INVERSE-SUSPENSION-SUSPENSION-C1 N A))
          (INVERSE-SUSPENSION-SUSPENSION-C1
               (+ N -1)
               (D-SUSPENSION-SUSPENSION-C1 N A)))))
       (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
              (INTEGERP N))
         (EQUAL (D-SUSPENSION-SUSPENSION-C1 (1- N)
                                            (D-SUSPENSION-SUSPENSION-C1 N A))
                (ZERO-SUSPENSION-SUSPENSION-C1 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-SUSPENSION-SUSPENSION-D1 N B)
                 (INV-SUSPENSION-SUSPENSION-D1 N C)
                 (INTEGERP N))
            (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                        C)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N A
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N B C))))
       (INV-SUSPENSION-SUSPENSION-D1 N (ZERO-SUSPENSION-SUSPENSION-D1 N))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N A (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (INVERSE-SUSPENSION-SUSPENSION-D1 N A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                            (ZERO-SUSPENSION-SUSPENSION-D1 N)))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1 N A)
                       B))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N A
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N B A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N R
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A)
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R B))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (ADDITION-RING-Z S R)
                                                      A)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N S A)
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (PRODUCT-RING-Z S R)
                                                      A)
                   (EXTERNAL-SUSPENSION-SUSPENSION-D1
                        N S
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (UNIT-Z)
                                                          A)
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N (INVERSE-SUSPENSION-SUSPENSION-D1 N A)
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N B))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N S A))
                       (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N S
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N S (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N))))
      (AND
       (AND
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                  (INTEGERP N))
             (INV-SUSPENSION-SUSPENSION-D1 (+ N -1)
                                           (D-SUSPENSION-SUSPENSION-D1 N A)))
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                  (INV-SUSPENSION-SUSPENSION-D1 N B)
                  (INTEGERP N))
             (EQUAL (D-SUSPENSION-SUSPENSION-D1
                         N
                         (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                         (+ N -1)
                         (D-SUSPENSION-SUSPENSION-D1 N A)
                         (D-SUSPENSION-SUSPENSION-D1 N B))))
        (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-SUSPENSION-SUSPENSION-D1
                             N
                             (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1
                             (+ N -1)
                             R (D-SUSPENSION-SUSPENSION-D1 N A))))
        (IMPLIES
         (INTEGERP N)
         (EQUAL
             (D-SUSPENSION-SUSPENSION-D1 N (ZERO-SUSPENSION-SUSPENSION-D1 N))
             (ZERO-SUSPENSION-SUSPENSION-D1 (+ N -1))))
        (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INTEGERP N))
         (EQUAL
          (D-SUSPENSION-SUSPENSION-D1 N
                                      (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
          (INVERSE-SUSPENSION-SUSPENSION-D1
               (+ N -1)
               (D-SUSPENSION-SUSPENSION-D1 N A)))))
       (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INTEGERP N))
         (EQUAL (D-SUSPENSION-SUSPENSION-D1 (1- N)
                                            (D-SUSPENSION-SUSPENSION-D1 N A))
                (ZERO-SUSPENSION-SUSPENSION-D1 (1- (1- N)))))))
     (AND
      (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                    (INTEGERP N))
               (INV-SUSPENSION-SUSPENSION-D1 N (LG-SUSPENSION N A)))
      (IMPLIES
        (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
             (INV-SUSPENSION-SUSPENSION-C1 N B)
             (INTEGERP N))
        (EQUAL
             (LG-SUSPENSION N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-C1 N A B))
             (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N (LG-SUSPENSION N A)
                                                       (LG-SUSPENSION N B))))
      (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
              (INV-RING-Z R)
              (INTEGERP N))
         (EQUAL (LG-SUSPENSION N
                               (EXTERNAL-SUSPENSION-SUSPENSION-C1 N R A))
                (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R (LG-SUSPENSION N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (LG-SUSPENSION N (ZERO-SUSPENSION-SUSPENSION-C1 N))
                      (ZERO-SUSPENSION-SUSPENSION-D1 N)))
      (IMPLIES
           (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                (INTEGERP N))
           (EQUAL (LG-SUSPENSION N
                                 (INVERSE-SUSPENSION-SUSPENSION-C1 N A))
                  (INVERSE-SUSPENSION-SUSPENSION-D1 N (LG-SUSPENSION N A)))))
     (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N A)
                   (INTEGERP N))
              (EQUAL (D-SUSPENSION-SUSPENSION-D1 N (LG-SUSPENSION N A))
                     (LG-SUSPENSION (1- N)
                                    (D-SUSPENSION-SUSPENSION-C1 N A)))))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N GNRT)
                  (INTEGERP N))
             (EQUAL (LF-SUSPENSION N (LG-SUSPENSION N GNRT))
                    GNRT))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                         N
                         (LH-SUSPENSION (1- N)
                                        (D-SUSPENSION-SUSPENSION-D1 N GNRT))
                         (D-SUSPENSION-SUSPENSION-D1 (1+ N)
                                                     (LH-SUSPENSION N GNRT)))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                         N GNRT
                         (INVERSE-SUSPENSION-SUSPENSION-D1
                              N
                              (LG-SUSPENSION N (LF-SUSPENSION N GNRT))))))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (LF-SUSPENSION (1+ N)
                                   (LH-SUSPENSION N GNRT))
                    (ZERO-SUSPENSION-SUSPENSION-C1 (1+ N))))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-C1 N GNRT)
                  (INTEGERP N))
             (EQUAL (LH-SUSPENSION N (LG-SUSPENSION N GNRT))
                    (ZERO-SUSPENSION-SUSPENSION-D1 (1+ N))))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (LH-SUSPENSION (1+ N)
                                   (LH-SUSPENSION N GNRT))
                    (ZERO-SUSPENSION-SUSPENSION-D1 (1+ (1+ N))))))
   (AND
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-SUSPENSION-SUSPENSION-D1 N B)
                 (INV-SUSPENSION-SUSPENSION-D1 N C)
                 (INTEGERP N))
            (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                        C)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N A
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N B C))))
       (INV-SUSPENSION-SUSPENSION-D1 N (ZERO-SUSPENSION-SUSPENSION-D1 N))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N A (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (INVERSE-SUSPENSION-SUSPENSION-D1 N A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                            (ZERO-SUSPENSION-SUSPENSION-D1 N)))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1 N A)
                       B))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N A
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N B A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N R
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A)
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R B))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (ADDITION-RING-Z S R)
                                                      A)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N S A)
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (PRODUCT-RING-Z S R)
                                                      A)
                   (EXTERNAL-SUSPENSION-SUSPENSION-D1
                        N S
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (UNIT-Z)
                                                          A)
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N (INVERSE-SUSPENSION-SUSPENSION-D1 N A)
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N B))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N S A))
                       (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N S
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N S (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N))))
      (AND
       (AND
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                  (INTEGERP N))
             (INV-SUSPENSION-SUSPENSION-D1 (+ N -1)
                                           (D-SUSPENSION-SUSPENSION-D1 N A)))
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                  (INV-SUSPENSION-SUSPENSION-D1 N B)
                  (INTEGERP N))
             (EQUAL (D-SUSPENSION-SUSPENSION-D1
                         N
                         (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                         (+ N -1)
                         (D-SUSPENSION-SUSPENSION-D1 N A)
                         (D-SUSPENSION-SUSPENSION-D1 N B))))
        (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-SUSPENSION-SUSPENSION-D1
                             N
                             (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1
                             (+ N -1)
                             R (D-SUSPENSION-SUSPENSION-D1 N A))))
        (IMPLIES
         (INTEGERP N)
         (EQUAL
             (D-SUSPENSION-SUSPENSION-D1 N (ZERO-SUSPENSION-SUSPENSION-D1 N))
             (ZERO-SUSPENSION-SUSPENSION-D1 (+ N -1))))
        (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INTEGERP N))
         (EQUAL
          (D-SUSPENSION-SUSPENSION-D1 N
                                      (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
          (INVERSE-SUSPENSION-SUSPENSION-D1
               (+ N -1)
               (D-SUSPENSION-SUSPENSION-D1 N A)))))
       (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INTEGERP N))
         (EQUAL (D-SUSPENSION-SUSPENSION-D1 (1- N)
                                            (D-SUSPENSION-SUSPENSION-D1 N A))
                (ZERO-SUSPENSION-SUSPENSION-D1 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-H1
                     N
                     (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B)))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                 (INV-SUSPENSION-SUSPENSION-H1 N B)
                 (INV-SUSPENSION-SUSPENSION-H1 N C)
                 (INTEGERP N))
            (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                        N
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B)
                        C)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                        N A
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N B C))))
       (INV-SUSPENSION-SUSPENSION-H1 N (ZERO-SUSPENSION-SUSPENSION-H1 N))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-H1
                     N
                     (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                            N A (ZERO-SUSPENSION-SUSPENSION-H1 N))
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-H1
                     N
                     (INVERSE-SUSPENSION-SUSPENSION-H1 N A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B)
                            (ZERO-SUSPENSION-SUSPENSION-H1 N)))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-H1 N A)
                       B))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                            N A
                            (INVERSE-SUSPENSION-SUSPENSION-H1 N A))
                       (ZERO-SUSPENSION-SUSPENSION-H1 N)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B)
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N B A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1
                            N R
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A)
                            (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R B))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1 N (ADDITION-RING-Z S R)
                                                      A)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                        N
                        (EXTERNAL-SUSPENSION-SUSPENSION-H1 N S A)
                        (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1 N (PRODUCT-RING-Z S R)
                                                      A)
                   (EXTERNAL-SUSPENSION-SUSPENSION-H1
                        N S
                        (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1 N (UNIT-Z)
                                                          A)
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-H1
                            N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                            N (INVERSE-SUSPENSION-SUSPENSION-H1 N A)
                            (INVERSE-SUSPENSION-SUSPENSION-H1 N B))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-H1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-H1 N S A))
                       (EXTERNAL-SUSPENSION-SUSPENSION-H1
                            N S
                            (INVERSE-SUSPENSION-SUSPENSION-H1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-H1
                            N (ZERO-SUSPENSION-SUSPENSION-H1 N))
                       (ZERO-SUSPENSION-SUSPENSION-H1 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1
                            N S (ZERO-SUSPENSION-SUSPENSION-H1 N))
                       (ZERO-SUSPENSION-SUSPENSION-H1 N))))
      (AND
       (AND
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                  (INTEGERP N))
             (INV-SUSPENSION-SUSPENSION-H1 (+ N -1)
                                           (D-SUSPENSION-SUSPENSION-H1 N A)))
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                  (INV-SUSPENSION-SUSPENSION-H1 N B)
                  (INTEGERP N))
             (EQUAL (D-SUSPENSION-SUSPENSION-H1
                         N
                         (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                         (+ N -1)
                         (D-SUSPENSION-SUSPENSION-H1 N A)
                         (D-SUSPENSION-SUSPENSION-H1 N B))))
        (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-SUSPENSION-SUSPENSION-H1
                             N
                             (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A))
                        (EXTERNAL-SUSPENSION-SUSPENSION-H1
                             (+ N -1)
                             R (D-SUSPENSION-SUSPENSION-H1 N A))))
        (IMPLIES
         (INTEGERP N)
         (EQUAL
             (D-SUSPENSION-SUSPENSION-H1 N (ZERO-SUSPENSION-SUSPENSION-H1 N))
             (ZERO-SUSPENSION-SUSPENSION-H1 (+ N -1))))
        (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
              (INTEGERP N))
         (EQUAL
          (D-SUSPENSION-SUSPENSION-H1 N
                                      (INVERSE-SUSPENSION-SUSPENSION-H1 N A))
          (INVERSE-SUSPENSION-SUSPENSION-H1
               (+ N -1)
               (D-SUSPENSION-SUSPENSION-H1 N A)))))
       (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
              (INTEGERP N))
         (EQUAL (D-SUSPENSION-SUSPENSION-H1 (1- N)
                                            (D-SUSPENSION-SUSPENSION-H1 N A))
                (ZERO-SUSPENSION-SUSPENSION-H1 (1- (1- N)))))))
     (AND
      (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                    (INTEGERP N))
               (INV-SUSPENSION-SUSPENSION-H1 N (RF-SUSPENSION N A)))
      (IMPLIES
        (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
             (INV-SUSPENSION-SUSPENSION-D1 N B)
             (INTEGERP N))
        (EQUAL
             (RF-SUSPENSION N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
             (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N (RF-SUSPENSION N A)
                                                       (RF-SUSPENSION N B))))
      (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INV-RING-Z R)
              (INTEGERP N))
         (EQUAL (RF-SUSPENSION N
                               (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))
                (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R (RF-SUSPENSION N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (RF-SUSPENSION N (ZERO-SUSPENSION-SUSPENSION-D1 N))
                      (ZERO-SUSPENSION-SUSPENSION-H1 N)))
      (IMPLIES
           (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                (INTEGERP N))
           (EQUAL (RF-SUSPENSION N
                                 (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
                  (INVERSE-SUSPENSION-SUSPENSION-H1 N (RF-SUSPENSION N A)))))
     (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                   (INTEGERP N))
              (EQUAL (D-SUSPENSION-SUSPENSION-H1 N (RF-SUSPENSION N A))
                     (RF-SUSPENSION (1- N)
                                    (D-SUSPENSION-SUSPENSION-D1 N A)))))
    (AND
     (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                   (INTEGERP N))
              (INV-SUSPENSION-SUSPENSION-D1 (+ N 1)
                                            (RH-SUSPENSION N A)))
     (IMPLIES
      (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
           (INV-SUSPENSION-SUSPENSION-D1 N B)
           (INTEGERP N))
      (EQUAL (RH-SUSPENSION N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
             (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 (+ N 1)
                                                       (RH-SUSPENSION N A)
                                                       (RH-SUSPENSION N B))))
     (IMPLIES
          (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (RH-SUSPENSION N
                                (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))
                 (EXTERNAL-SUSPENSION-SUSPENSION-D1 (+ N 1)
                                                    R (RH-SUSPENSION N A))))
     (IMPLIES (INTEGERP N)
              (EQUAL (RH-SUSPENSION N (ZERO-SUSPENSION-SUSPENSION-D1 N))
                     (ZERO-SUSPENSION-SUSPENSION-D1 (+ N 1))))
     (IMPLIES
          (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
               (INTEGERP N))
          (EQUAL (RH-SUSPENSION N
                                (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
                 (INVERSE-SUSPENSION-SUSPENSION-D1 (+ N 1)
                                                   (RH-SUSPENSION N A)))))
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-H1
                     N
                     (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B)))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                 (INV-SUSPENSION-SUSPENSION-H1 N B)
                 (INV-SUSPENSION-SUSPENSION-H1 N C)
                 (INTEGERP N))
            (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                        N
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B)
                        C)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                        N A
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N B C))))
       (INV-SUSPENSION-SUSPENSION-H1 N (ZERO-SUSPENSION-SUSPENSION-H1 N))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-H1
                     N
                     (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                            N A (ZERO-SUSPENSION-SUSPENSION-H1 N))
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-H1
                     N
                     (INVERSE-SUSPENSION-SUSPENSION-H1 N A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B)
                            (ZERO-SUSPENSION-SUSPENSION-H1 N)))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-H1 N A)
                       B))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                            N A
                            (INVERSE-SUSPENSION-SUSPENSION-H1 N A))
                       (ZERO-SUSPENSION-SUSPENSION-H1 N)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B)
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N B A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1
                            N R
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A)
                            (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R B))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1 N (ADDITION-RING-Z S R)
                                                      A)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                        N
                        (EXTERNAL-SUSPENSION-SUSPENSION-H1 N S A)
                        (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1 N (PRODUCT-RING-Z S R)
                                                      A)
                   (EXTERNAL-SUSPENSION-SUSPENSION-H1
                        N S
                        (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1 N (UNIT-Z)
                                                          A)
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-SUSPENSION-SUSPENSION-H1 N B)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-H1
                            N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                            N (INVERSE-SUSPENSION-SUSPENSION-H1 N A)
                            (INVERSE-SUSPENSION-SUSPENSION-H1 N B))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-H1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-H1 N S A))
                       (EXTERNAL-SUSPENSION-SUSPENSION-H1
                            N S
                            (INVERSE-SUSPENSION-SUSPENSION-H1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-H1
                            N (ZERO-SUSPENSION-SUSPENSION-H1 N))
                       (ZERO-SUSPENSION-SUSPENSION-H1 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-H1
                            N S (ZERO-SUSPENSION-SUSPENSION-H1 N))
                       (ZERO-SUSPENSION-SUSPENSION-H1 N))))
      (AND
       (AND
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                  (INTEGERP N))
             (INV-SUSPENSION-SUSPENSION-H1 (+ N -1)
                                           (D-SUSPENSION-SUSPENSION-H1 N A)))
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                  (INV-SUSPENSION-SUSPENSION-H1 N B)
                  (INTEGERP N))
             (EQUAL (D-SUSPENSION-SUSPENSION-H1
                         N
                         (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1
                         (+ N -1)
                         (D-SUSPENSION-SUSPENSION-H1 N A)
                         (D-SUSPENSION-SUSPENSION-H1 N B))))
        (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-SUSPENSION-SUSPENSION-H1
                             N
                             (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A))
                        (EXTERNAL-SUSPENSION-SUSPENSION-H1
                             (+ N -1)
                             R (D-SUSPENSION-SUSPENSION-H1 N A))))
        (IMPLIES
         (INTEGERP N)
         (EQUAL
             (D-SUSPENSION-SUSPENSION-H1 N (ZERO-SUSPENSION-SUSPENSION-H1 N))
             (ZERO-SUSPENSION-SUSPENSION-H1 (+ N -1))))
        (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
              (INTEGERP N))
         (EQUAL
          (D-SUSPENSION-SUSPENSION-H1 N
                                      (INVERSE-SUSPENSION-SUSPENSION-H1 N A))
          (INVERSE-SUSPENSION-SUSPENSION-H1
               (+ N -1)
               (D-SUSPENSION-SUSPENSION-H1 N A)))))
       (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
              (INTEGERP N))
         (EQUAL (D-SUSPENSION-SUSPENSION-H1 (1- N)
                                            (D-SUSPENSION-SUSPENSION-H1 N A))
                (ZERO-SUSPENSION-SUSPENSION-H1 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-SUSPENSION-SUSPENSION-D1 N B)
                 (INV-SUSPENSION-SUSPENSION-D1 N C)
                 (INTEGERP N))
            (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                        C)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N A
                        (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N B C))))
       (INV-SUSPENSION-SUSPENSION-D1 N (ZERO-SUSPENSION-SUSPENSION-D1 N))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N A (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (INV-SUSPENSION-SUSPENSION-D1
                     N
                     (INVERSE-SUSPENSION-SUSPENSION-D1 N A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                            (ZERO-SUSPENSION-SUSPENSION-D1 N)))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1 N A)
                       B))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N A
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B)
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N B A)))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N R
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A)
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R B))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (ADDITION-RING-Z S R)
                                                      A)
                   (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                        N
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N S A)
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))))
       (IMPLIES
            (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (PRODUCT-RING-Z S R)
                                                      A)
                   (EXTERNAL-SUSPENSION-SUSPENSION-D1
                        N S
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1 N (UNIT-Z)
                                                          A)
                       A))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-SUSPENSION-SUSPENSION-D1 N B)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                       (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                            N (INVERSE-SUSPENSION-SUSPENSION-D1 N A)
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N B))))
       (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N
                            (EXTERNAL-SUSPENSION-SUSPENSION-D1 N S A))
                       (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N S
                            (INVERSE-SUSPENSION-SUSPENSION-D1 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-SUSPENSION-SUSPENSION-D1
                            N (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-SUSPENSION-SUSPENSION-D1
                            N S (ZERO-SUSPENSION-SUSPENSION-D1 N))
                       (ZERO-SUSPENSION-SUSPENSION-D1 N))))
      (AND
       (AND
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                  (INTEGERP N))
             (INV-SUSPENSION-SUSPENSION-D1 (+ N -1)
                                           (D-SUSPENSION-SUSPENSION-D1 N A)))
        (IMPLIES
             (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                  (INV-SUSPENSION-SUSPENSION-D1 N B)
                  (INTEGERP N))
             (EQUAL (D-SUSPENSION-SUSPENSION-D1
                         N
                         (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N A B))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                         (+ N -1)
                         (D-SUSPENSION-SUSPENSION-D1 N A)
                         (D-SUSPENSION-SUSPENSION-D1 N B))))
        (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-SUSPENSION-SUSPENSION-D1
                             N
                             (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R A))
                        (EXTERNAL-SUSPENSION-SUSPENSION-D1
                             (+ N -1)
                             R (D-SUSPENSION-SUSPENSION-D1 N A))))
        (IMPLIES
         (INTEGERP N)
         (EQUAL
             (D-SUSPENSION-SUSPENSION-D1 N (ZERO-SUSPENSION-SUSPENSION-D1 N))
             (ZERO-SUSPENSION-SUSPENSION-D1 (+ N -1))))
        (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INTEGERP N))
         (EQUAL
          (D-SUSPENSION-SUSPENSION-D1 N
                                      (INVERSE-SUSPENSION-SUSPENSION-D1 N A))
          (INVERSE-SUSPENSION-SUSPENSION-D1
               (+ N -1)
               (D-SUSPENSION-SUSPENSION-D1 N A)))))
       (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-D1 N A)
              (INTEGERP N))
         (EQUAL (D-SUSPENSION-SUSPENSION-D1 (1- N)
                                            (D-SUSPENSION-SUSPENSION-D1 N A))
                (ZERO-SUSPENSION-SUSPENSION-D1 (1- (1- N)))))))
     (AND
      (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                    (INTEGERP N))
               (INV-SUSPENSION-SUSPENSION-D1 N (RG-SUSPENSION N A)))
      (IMPLIES
        (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
             (INV-SUSPENSION-SUSPENSION-H1 N B)
             (INTEGERP N))
        (EQUAL
             (RG-SUSPENSION N
                            (GROUP-OPERATION-SUSPENSION-SUSPENSION-H1 N A B))
             (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1 N (RG-SUSPENSION N A)
                                                       (RG-SUSPENSION N B))))
      (IMPLIES
         (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
              (INV-RING-Z R)
              (INTEGERP N))
         (EQUAL (RG-SUSPENSION N
                               (EXTERNAL-SUSPENSION-SUSPENSION-H1 N R A))
                (EXTERNAL-SUSPENSION-SUSPENSION-D1 N R (RG-SUSPENSION N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (RG-SUSPENSION N (ZERO-SUSPENSION-SUSPENSION-H1 N))
                      (ZERO-SUSPENSION-SUSPENSION-D1 N)))
      (IMPLIES
           (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                (INTEGERP N))
           (EQUAL (RG-SUSPENSION N
                                 (INVERSE-SUSPENSION-SUSPENSION-H1 N A))
                  (INVERSE-SUSPENSION-SUSPENSION-D1 N (RG-SUSPENSION N A)))))
     (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N A)
                   (INTEGERP N))
              (EQUAL (D-SUSPENSION-SUSPENSION-D1 N (RG-SUSPENSION N A))
                     (RG-SUSPENSION (1- N)
                                    (D-SUSPENSION-SUSPENSION-H1 N A)))))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N GNRT)
                  (INTEGERP N))
             (EQUAL (RF-SUSPENSION N (RG-SUSPENSION N GNRT))
                    GNRT))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                         N
                         (RH-SUSPENSION (1- N)
                                        (D-SUSPENSION-SUSPENSION-D1 N GNRT))
                         (D-SUSPENSION-SUSPENSION-D1 (1+ N)
                                                     (RH-SUSPENSION N GNRT)))
                    (GROUP-OPERATION-SUSPENSION-SUSPENSION-D1
                         N GNRT
                         (INVERSE-SUSPENSION-SUSPENSION-D1
                              N
                              (RG-SUSPENSION N (RF-SUSPENSION N GNRT))))))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (RF-SUSPENSION (1+ N)
                                   (RH-SUSPENSION N GNRT))
                    (ZERO-SUSPENSION-SUSPENSION-H1 (1+ N))))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-H1 N GNRT)
                  (INTEGERP N))
             (EQUAL (RH-SUSPENSION N (RG-SUSPENSION N GNRT))
                    (ZERO-SUSPENSION-SUSPENSION-D1 (1+ N))))
    (IMPLIES (AND (INV-SUSPENSION-SUSPENSION-D1 N GNRT)
                  (INTEGERP N))
             (EQUAL (RH-SUSPENSION (1+ N)
                                   (RH-SUSPENSION N GNRT))
                    (ZERO-SUSPENSION-SUSPENSION-D1 (1+ (1+ N))))))))))


(make-generic-theory *suspension-REDUCTION-THEOREM*)


